Nuprl Lemma : R-discrete_compat_wf 11,40
A,B:es_realizer{i:l}. R-discrete_compat(A; B)  prop{i:l} 
latex

Definitionsx. t(x), ff, tt, P  Q, if b then t else f fi , R-discrete_compat(A; B), prop{i:l}, t  T, es_realizer{i:l}, x:A. B(x), x(s), P  Q, P  Q, Unit, ,
Lemmasfinite-prob-space wf, decl-type wf, decl-state wf, fpf wf, IdLnk wf, Knd wf, rationals wf, unit wf, true wf, Rinit-discrete wf, Rinit-x wf, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Reffect-discrete wf, Reffect-x wf, Id wf, eqtt to assert, bool wf, Reffect? wf

origin